(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 12)) (_ BitVec 11))
(declare-fun f1 ( (_ BitVec 2) (_ BitVec 11)) (_ BitVec 4))
(declare-fun p0 ( (_ BitVec 13) (_ BitVec 8) (_ BitVec 2)) Bool)
(declare-fun p1 ( (_ BitVec 14) (_ BitVec 5)) Bool)
(declare-fun v0 () (_ BitVec 7))
(declare-fun v1 () (_ BitVec 12))
(declare-fun v2 () (_ BitVec 2))
(assert (let ((e3(_ bv45 6)))
(let ((e4(_ bv25 6)))
(let ((e5 (f0 ((_ zero_extend 5) v0))))
(let ((e6 (f1 ((_ extract 3 2) v1) ((_ sign_extend 5) e3))))
(let ((e7 (ite (p1 ((_ sign_extend 8) e3) ((_ sign_extend 1) e6)) (_ bv1 1) (_ bv0 1))))
(let ((e8 (bvneg e6)))
(let ((e9 (bvsrem v2 v2)))
(let ((e10 (ite (p0 ((_ zero_extend 7) e3) ((_ extract 10 3) e5) ((_ extract 7 6) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e11 ((_ zero_extend 4) e8)))
(let ((e12 (ite (bvsge ((_ zero_extend 8) e6) v1) (_ bv1 1) (_ bv0 1))))
(let ((e13 (bvadd ((_ zero_extend 3) e12) e6)))
(let ((e14 ((_ sign_extend 6) e9)))
(let ((e15 (bvnor ((_ sign_extend 1) v0) e14)))
(let ((e16 (ite (bvult ((_ zero_extend 2) e3) e14) (_ bv1 1) (_ bv0 1))))
(let ((e17 (bvneg e16)))
(let ((e18 ((_ sign_extend 10) e17)))
(let ((e19 (ite (distinct ((_ zero_extend 3) e8) v0) (_ bv1 1) (_ bv0 1))))
(let ((e20 (bvudiv ((_ zero_extend 3) e16) e13)))
(let ((e21 (bvudiv e13 e8)))
(let ((e22 (ite (= (_ bv1 1) ((_ extract 1 1) e6)) v1 ((_ sign_extend 8) e13))))
(let ((e23 (bvxnor ((_ sign_extend 5) e19) e4)))
(let ((e24 (bvsge ((_ sign_extend 11) e7) v1)))
(let ((e25 (distinct e13 ((_ zero_extend 3) e10))))
(let ((e26 (= e8 ((_ sign_extend 2) e9))))
(let ((e27 (p0 ((_ zero_extend 9) e13) ((_ sign_extend 4) e8) e9)))
(let ((e28 (bvslt ((_ sign_extend 2) e13) e23)))
(let ((e29 (bvsgt e23 ((_ zero_extend 5) e16))))
(let ((e30 (p1 ((_ zero_extend 13) e17) ((_ sign_extend 1) e8))))
(let ((e31 (= e22 ((_ sign_extend 4) e15))))
(let ((e32 (bvsgt ((_ sign_extend 10) v2) e22)))
(let ((e33 (bvsle e3 ((_ zero_extend 2) e20))))
(let ((e34 (bvule ((_ sign_extend 3) e19) e6)))
(let ((e35 (bvugt e10 e17)))
(let ((e36 (bvslt e5 ((_ sign_extend 3) e11))))
(let ((e37 (bvsle e21 ((_ zero_extend 3) e10))))
(let ((e38 (= e13 e21)))
(let ((e39 (bvsge ((_ zero_extend 2) e20) e4)))
(let ((e40 (bvslt e3 ((_ zero_extend 2) e13))))
(let ((e41 (bvule e4 ((_ sign_extend 5) e17))))
(let ((e42 (bvsge e8 e8)))
(let ((e43 (bvslt e22 e22)))
(let ((e44 (bvslt e15 e11)))
(let ((e45 (bvule ((_ zero_extend 7) e20) e5)))
(let ((e46 (p0 ((_ zero_extend 12) e10) ((_ extract 9 2) e22) ((_ extract 3 2) e8))))
(let ((e47 (bvsgt v0 ((_ zero_extend 6) e12))))
(let ((e48 (bvsle e15 e11)))
(let ((e49 (distinct ((_ sign_extend 4) e9) e4)))
(let ((e50 (bvslt e6 ((_ zero_extend 3) e10))))
(let ((e51 (bvsle e5 ((_ sign_extend 10) e12))))
(let ((e52 (bvslt ((_ zero_extend 2) e13) e3)))
(let ((e53 (bvsge ((_ zero_extend 3) e17) e13)))
(let ((e54 (bvslt e16 e16)))
(let ((e55 (bvugt e11 ((_ zero_extend 1) v0))))
(let ((e56 (bvuge ((_ sign_extend 6) e7) v0)))
(let ((e57 (= ((_ sign_extend 1) e18) v1)))
(let ((e58 (p0 ((_ sign_extend 11) e9) ((_ extract 8 1) e22) ((_ extract 5 4) e4))))
(let ((e59 (bvsge e4 ((_ zero_extend 2) e6))))
(let ((e60 (distinct e18 ((_ sign_extend 9) e9))))
(let ((e61 (p0 ((_ zero_extend 9) e8) ((_ extract 10 3) e5) ((_ extract 3 2) e6))))
(let ((e62 (bvult ((_ zero_extend 8) e21) e22)))
(let ((e63 (bvult v2 ((_ sign_extend 1) e16))))
(let ((e64 (bvsge e15 ((_ zero_extend 4) e20))))
(let ((e65 (p0 ((_ sign_extend 9) e6) ((_ extract 9 2) v1) ((_ extract 6 5) e22))))
(let ((e66 (distinct e18 ((_ zero_extend 10) e10))))
(let ((e67 (p1 ((_ sign_extend 6) e11) ((_ zero_extend 4) e17))))
(let ((e68 (bvuge e18 ((_ zero_extend 7) e20))))
(let ((e69 (bvult e4 e23)))
(let ((e70 (p0 ((_ sign_extend 1) v1) ((_ zero_extend 4) e6) ((_ extract 3 2) e11))))
(let ((e71 (distinct ((_ sign_extend 2) e23) e11)))
(let ((e72 (distinct e15 ((_ zero_extend 7) e10))))
(let ((e73 (distinct ((_ sign_extend 3) e7) e13)))
(let ((e74 (bvule e4 ((_ sign_extend 5) e17))))
(let ((e75 (distinct ((_ sign_extend 8) e21) e22)))
(let ((e76 (bvuge ((_ sign_extend 1) e5) v1)))
(let ((e77 (bvsge e6 ((_ zero_extend 2) e9))))
(let ((e78 (bvslt e12 e10)))
(let ((e79 (bvsgt ((_ zero_extend 7) e17) e11)))
(let ((e80 (bvugt ((_ sign_extend 3) e12) e21)))
(let ((e81 (bvsgt ((_ zero_extend 5) e10) e4)))
(let ((e82 (bvule ((_ sign_extend 1) e10) e9)))
(let ((e83 (bvuge ((_ sign_extend 2) e23) e14)))
(let ((e84 (not e28)))
(let ((e85 (or e71 e44)))
(let ((e86 (not e30)))
(let ((e87 (or e25 e55)))
(let ((e88 (ite e36 e63 e29)))
(let ((e89 (xor e52 e43)))
(let ((e90 (not e47)))
(let ((e91 (= e83 e35)))
(let ((e92 (ite e53 e73 e75)))
(let ((e93 (or e41 e80)))
(let ((e94 (xor e64 e51)))
(let ((e95 (ite e50 e94 e78)))
(let ((e96 (xor e81 e34)))
(let ((e97 (ite e46 e67 e37)))
(let ((e98 (=> e48 e87)))
(let ((e99 (ite e56 e38 e74)))
(let ((e100 (xor e91 e86)))
(let ((e101 (xor e62 e89)))
(let ((e102 (ite e27 e79 e61)))
(let ((e103 (and e32 e95)))
(let ((e104 (xor e45 e90)))
(let ((e105 (xor e104 e96)))
(let ((e106 (=> e85 e101)))
(let ((e107 (= e82 e98)))
(let ((e108 (=> e42 e88)))
(let ((e109 (not e99)))
(let ((e110 (and e102 e97)))
(let ((e111 (and e105 e106)))
(let ((e112 (=> e103 e77)))
(let ((e113 (and e92 e33)))
(let ((e114 (or e68 e68)))
(let ((e115 (and e24 e110)))
(let ((e116 (not e93)))
(let ((e117 (not e40)))
(let ((e118 (not e109)))
(let ((e119 (or e70 e112)))
(let ((e120 (not e107)))
(let ((e121 (= e115 e113)))
(let ((e122 (ite e65 e65 e60)))
(let ((e123 (not e54)))
(let ((e124 (not e39)))
(let ((e125 (not e118)))
(let ((e126 (ite e108 e59 e117)))
(let ((e127 (ite e124 e116 e69)))
(let ((e128 (not e76)))
(let ((e129 (not e122)))
(let ((e130 (= e129 e119)))
(let ((e131 (=> e66 e58)))
(let ((e132 (ite e57 e84 e31)))
(let ((e133 (or e121 e131)))
(let ((e134 (ite e130 e120 e100)))
(let ((e135 (=> e111 e114)))
(let ((e136 (and e127 e49)))
(let ((e137 (and e128 e125)))
(let ((e138 (not e135)))
(let ((e139 (and e26 e133)))
(let ((e140 (ite e137 e72 e134)))
(let ((e141 (=> e123 e136)))
(let ((e142 (and e126 e138)))
(let ((e143 (xor e140 e132)))
(let ((e144 (= e143 e142)))
(let ((e145 (and e139 e144)))
(let ((e146 (and e145 e141)))
(let ((e147 (and e146 (not (= v2 (_ bv0 2))))))
(let ((e148 (and e147 (not (= v2 (bvnot (_ bv0 2)))))))
(let ((e149 (and e148 (not (= e13 (_ bv0 4))))))
(let ((e150 (and e149 (not (= e8 (_ bv0 4))))))
e150
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
